p:FinProbSpace, n:, X, Y:RandomVariable(p;n), a:.
rv-disjoint(p;n;X;Y)  rv-disjoint(p;n;X;a*Y) 

latex

Definitions	FinProbSpace, t  T, , x:A. B(x), RandomVariable(p;n), , P  Q, False, A, A  B, , {x:A| B(x)} , r * s, (x.F(x)) o X, rv-disjoint(p;n;X;Y), x.A(x), x. t(x), Void, x:A.B(x), Top, type List, x:AB(x), S  T, P & Q, i  j < k, {i..j}, ||as||, #$n, f(a), q*X, s = t, True, <a, b>, T
Lemmas	squash wf, true wf, int seg wf, length wf nat, top wf, rv-disjoint-compose, qmul wf, rv-disjoint wf, rationals wf, random-variable wf, nat wf, finite-prob-space wf